# sumn_mcy
## Введение

Тестирование стенда с использованием мутаций с помощью MCY (Mutation Coverage with Yosys)

В этом проекте представлен пример тестирования отладочного стенда для модуля sum_n. 

Описание формального тестирования модуля sum_n вы можете посмотреть в статье [К формальной проверке][1] на fpga-systems.ru. Проект формального тестирования можно взять [от сюда][2].

## Как использовать

Клонируйте репу
```bash
$ git clone https://gitverse.ru/sc/serge.balakshiy/sumn_mcy.git
```
Сгенерируйте проект. Выполните 
```bash
$ sh sumn
```
Получите помощь
```bash
make help
```
Возможно вам необходимо будет установить переменную SCRIPTS. 
Укажите свой путь.
```bash
$ export SCRIPTS=/usr/local/share/mcy/scripts
```
## Выполните тестирование созданного проекта
Вы можете делать это по частям:
Убедитесь в том, что testbench работает
```bash
make tb
```
Если у вас установлен gtkwave, то вы сразу увидете эпюры.

Чтобы очистить артефакты testbench выполните
```bash
make clean_tb
```
## Проверка тестовой среды
Выполните проверку работоспособности тестовой среды
```bash
$ make sim
```
Выполните проверку работоспособности теста на эквивалентность
```bash
$ make eq
```
либо вместе
```bash
$ make sim eq
```
Получите
```bash
DONE (PASS, rc=0)
```
## Настройка testbench
По умолчанию testbench создает наборы данных генерируя их случайным образом. Это создаст довольно много мутаций.
Для отладки вы можете ускорить работу заменив наборы данных в testbench на пред установленные вручную. Тогда выполните
```bash
$ make sim_hand
```
Вернуть обратно можно либо заново перегенерировав проект, либо выполните
```bash
$ make sim_rand
```
Это снова включит случайную генерацию наборов данных в testbench.

Также вы можете захотеть изменить количество наборов данных для работы стенда. Тогда откройте файл sumn_sim_tb.v и в строке
```verilog
   initial begin
      repeat(77) begin
```
укажите нужное вам количество повторений.

Кроме того в файле config.mcy в строке
```bash
[options]
size 21
```
установите нужное вам количество мутаций. Рекомендуется ~1000

Все настройки будут действительны только на текущий сеанс, пока вы не перегенерируете проект. См. пункт [Как изменять](#как-изменять) 
## Работа с mcy
Почистите базу данных теста
```bash
$ make purge
mcy purge
==> Purge database
  -> Reading configuration file.
  -> Remove 'tasks' subdirectory.
  -> Remove 'database' subdirectory.
```
Снова инициируйте новую базу данных
```bash
$ make init
mcy init
==> Initialize database
  -> Reading configuration file.
  -> Checking database existance.
  -> Creating database directory.
  -> Creating design script file.
  -> Creating design RTL.
yosys -ql database/design.log database/design.ys
  -> Creating mutations script file.
  -> Creating mutations.
yosys -ql database/mutations.log database/mutations.ys
  -> Initializing database.
  -> Connecting to database.
  -> Importing mutations.
  -> Importing design sources.
  -> Reseting database statistics.
  -> Remove 'tasks' subdirectory.
  -> Update mutations.
  -> Getting database statistics.
Database contains 0 cached results.
Queued 10 "test_sumn_sim" tests.
```
Выполните тесты
```bash
$ make mcy_run
mcy run
==> Run all tasks from queue
  -> Reading configuration file.
  -> Connecting to database.
  ==> Running task aff9432a-f0fe-4044-a612-3cd6ee78d50c (test_sumn_sim)
 1 1 mutate -mode none
...
  ==> Finishing task 2ee72e7b-7f64-4f0f-bae8-218cbf5bbbfd (test_sumn_eq)
  1 10 PASS mutate -mode cnot1 -module sumn -cell $div$sumn.v:9$10 -port Y -portbit 0 -ctrlbit 17 -src sumn.v:9.50-9.87
  -> Finished running all tasks.
  -> Getting database statistics.
Database contains 20 cached results.
Database contains 8 cached "FAIL" results for "test_sumn_eq".
Database contains 2 cached "PASS" results for "test_sumn_eq".
Database contains 8 cached "FAIL" results for "test_sumn_sim".
Database contains 2 cached "PASS" results for "test_sumn_sim".
Tagged 8 mutations as "COVERED".
Tagged 2 mutations as "NOCHANGE".
  -> Print report
Coverage: 100.00%
```
Иногда на мутациях бывает FAIL. Разберитесь и снова повторите
```bash
$ make purge
$ make init
$ make mcy_run
```
## Второй путь
После того как вы развернёте проект, просто вызывайте mcy
```bash
$ mcy purge
$ mcy init
$ mcy run
```
## Отображение статистики
После завершения mcy run вы получите что-то такое:
```bash
...
  -> Finished running all tasks.
  -> Getting database statistics.
Database contains 48 cached results.
Database contains 16 cached "FAIL" results for "test_sumn_eq".
Database contains 5 cached "PASS" results for "test_sumn_eq".
Database contains 6 cached "PASS" results for "test_sumn_fm".
Database contains 15 cached "FAIL" results for "test_sumn_sim".
Database contains 6 cached "PASS" results for "test_sumn_sim".
Tagged 15 mutations as "COVERED".
Tagged 5 mutations as "NOCHANGE".
Tagged 1 mutations as "UNCOVERED".
  -> Print report
Coverage: 93.75%
```
Уточнить покрытие можно командой 
```bash
$ mcy source sumn.v
==> Retrieving source info
  -> Reading configuration file.
  -> Connecting to database.
  -> Extract coverage info.
  -> Display source file with info.
     |	module sumn
     |	  (
     |	   // input wire
     |	   input wire [7:0]   m_in, n_in,
     |	   // output wire
    5|	   output wire [15:0] s_out
     |	   );
     |	
!  -1|	   assign s_out = (n_in>=m_in)&(n_in>0)&(m_in>0)?(m_in + n_in) * (n_in - m_in + 1) / 2:0;   
```
Положительные числа в левом столбце указывают на мутации, помеченные как COVERED, отрицательные числа указывают на UNCOVERED.

Также во время mcy run, в случае долгого теста вы можете выполнить в другом терминале и в корневом каталоге проекта
```bash
$ mcy dash
... 
   Use a production WSGI server instead.
 * Debug mode: on
WARNING: This is a development server. Do not use it in a production deployment. Use a production WSGI server instead.
 * Running on http://127.0.0.1:5000
```
Откройте указанный адрес в своём браузере, чтобы следить за ходом выполнения на панели мониторинга. Это можно делать и при выполнении тестов на удалённом сервере.

Для более подробного визуального изучения мутаций можно открыть
```bash
$ mcy gui
```
Здесь вы увидите "горячие точки" вашего кода, где существуют пробелы в покрытии. На данный момент это жёстко запрограммировано для использования имён тегов «COVERED» и «UNCOVERED».

## Как изменять

Вы можете вносить изменения в файлы: config.mcy, *.sv, *.v, *.sby, *.ys, *.sh кроме sumn. Но эти изменения будут текущими и не будут сохранены при выполнении sh sumn. 

Если вы хотите фиксировать изменения то внесите изменения в sumn. Все файлы проекта будут перегенерированы при выполнении 
```bash
sh sumn
```
а также при выполнении
```bash
$ make
```

## Развивайте проект.

<!--Reference links in article-->
[1]: https://fpga-systems.ru/publ/raznoe/poznavatelnoe/k_formalnoj_proverke/16-1-0-224
[2]: https://gitverse.ru/serge.balakshiy/sum_n